COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00007 ENDMK
C⊗;

.DEVICE XGP
.FONT 4 "BASB30"
.FONT 3 "BASI30"
.FONT 2 "BDR30"
.FONT 1 "BDR30"
.EVENLEFTBORDER←ODDLEFTBORDER←1000
.PAGE FRAME 52 HIGH 83 WIDE;
.AREA TEXT LINES 4 TO 50;
.TITLE AREA HEADING LINES 1 TO 3;
.PLACE TEXT;
.EVERY HEADING(,,{PAGE});
.BEGIN NOFILL
.VARIABLE CHW
.CHW ← CHARW
.TURN OFF "βα#\←∞↑↓∪"
.TURN ON "∂{%"
.TURN ON "/" FOR "α"
.AT "∂∂(" CH ")" ⊂ CHARW←CH}∂(2){CHARW←CHW ⊃


∂∂(48)%3samefringe%2[%3x%2, %3y%2] ← [¬%4at %3x%2 ∧ ¬%4at %3y%2 ∧ %3same%2[%4a %3x%2, %4a %3y%2, %4d %3x%2, %4d %3y%2]] ∨ %3x%2 %4eq %3y



∂∂(48)same%2[%3x%2, %3y%2, %3u%2, %3v%2] ← 
∂∂(80)[¬%4at %3x%2 ∧ ¬%4at %3y%2 ∧ %3same%2[%4a %3x%2, %4a %3y%2, %4d %3x%2 . %3u%2, %4d %3y%2 . %3v%2]]
∂∂(80)∨ [¬%4at %3y%2 ∧ %3same%2[%3x%2, %4a %3y%2, %3u%2, %4d %3y%2 . %3v%2]]
∂∂(80)∨ [¬%4at %3x%2 ∧ %3same%2[%4a %3x%2, %3y%2, %4d %3x%2 . %3u%2, %3v%2]]
∂∂(80)∨ [%3x%2 %4eq %3y%2 ∧ %3samefringe%2[%3u%2, %3v%2]]



∂∂(48)%3samefringe1%2[%3x%2, %3y%2] ← %3x%2 %4eq %3y%2 ∨ [¬%4at %3x%2 ∧ ¬%4at %3y%2 ∧ %3same1%2[%4a %3x%2, %4a %3y%2, %4d %3x%2, %4d %3y%2]]



∂∂(48)%3same1%2[%3x%2, %3y%2, %3u%2, %3v%2] ← 
∂∂(80)%4if%2 %4at %3x%2 %4then%2 [%4if%2 %4at %3y%2 %4then%2 %3x%2 %4eq %3y%2 ∧ %3samefringe1%2[%3u%2, %3v%2] %4else%2 %3same1%2[%3x%2, %4a %3y%2, %3u%2, %4d %3y%2 . %3v%2]]
∂∂(80)%4else if%2 %4at %3y%2 %4then%2 %3same1%2[%4a %3x%2, %3y%2, %4d %3x%2 . %3u%2, %3v%2]
∂∂(80)%4else%2 %3same1%2[%4a %3x%2, %4a %3y%2, %4d %3x%2 . %3u%2, %4d %3y%2 . %3v%2]



∂∂(48)%3samefringe2%2[%3x%2, %3y%2] ← %3same2%2[%3abot%2 <%3x%2>, %3abot%2 <%3y%2>]



∂∂(48)%3same2%2[%3u%2, %3v%2] ← [%4n %3u%2 ∧ %4n %3v%2] ∨ [¬%4n %3u%2 ∧ ¬%4n %3v%2 ∧ %4a %3u%2 %4eq a %3v%2 ∧ %3same2%2[%3next%2 %3u%2, %3next%2 %3v%2]]



∂∂(48)%3next%2 %3u%2 ← %4if%2 %4n %3u%2 %4then%2 NIL %4else if%2 %4ad %3u%2 %4eq %3'a%2 %4then%2 %3abot%2 %4dadd %3u%2 . [%3'd%2 . %4dd %3u%2] %4else%2 %3next%2 %4dd %3u



∂∂(48)abot%2 %3u%2 ← %4if%2 %4at a %3u%2 %4then%2 %3u%2 %4else%2 %3abot%2 %4aa %3u%2 . [%3'a%2 . %3u%2]



∂∂(48)%3samefringe3%2[%3x%2, %3y%2] ← 
∂∂(80)%3x%2 %4eq %3y%2 ∨ [¬%4at %3x%2 ∧ ¬%4at %3y%2 ∧ /{%3digatom%2 %3x%2, %3digatom%2 %3y%2}[λ%3u%2, %3v%2. %4a %3u%2 %4eq a %3v%2 ∧ %3samefringe3%2[%4d %3u%2, %4d %3v%2]]]



∂∂(48)%3samefringe4%2[%3x%2, %3y%2] ← %3x%2 %4eq %3y%2 ∨ [¬%4at %3x%2 ∧ ¬%4at %3y%2 ∧ %3same4%2[%3digatom%2 %3x%2, %3digatom%2 %3y%2]]



∂∂(48)%3same4%2[%3x%2, %3y%2] ← %4a %3x%2 %4eq a %3y%2 ∧ %3samefringe4%2[%4d %3x%2, %4d %3y%2]



∂∂(48)%3digatom%2 %3u%2 ← %4if%2 %4at a %3u%2 %4then%2 %3u%2 %4else%2 %3digatom%2 %4aa %3u%2 . [%4da %3u%2 . %4d %3u%2]

.END